Inference at * 1 1 1 
Iof proof for Lemma bool sq:

.....assertion..... NILNIL

1. x : ?Unit
2. y : ?Unit
3. x = y
4. case x of inl(x) => x | inr(x) => x = case y of inl(x) => x | inr(x) => x
5. case x of inl(x) => True | inr(x) => False = case y of inl(x) => True | inr(x) => False
  (True = False) 

latex

 by ((D 0) 
THENW ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
T) inil_term))) 

latex

T1: 

T1: 6. True = False
T1:   False
T.

Definitions	t  T, P  Q, A,
Lemmas	false wf, true wf